ff $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr $\cdot$